////////////////////////////////////////////////////////////////////////////////
// This file is part of the Mist compiler.                                    //
//                                                                            //
// Copyright (C) 2009 The Mist project                                        //
//                                                                            //
// For a list of contributors, see the COMMITTERS file.                       //
//                                                                            //
// The Mist compiler is free software: you can redistribute it and/or modify  //
// it under the terms of the GNU General Public License as published by       //
// the Free Software Foundation, either version 3 of the License, or          //
// (at your option) any later version.                                        //
//                                                                            //
// The Mist compiler is distributed in the hope that it will be useful,       //
// but WITHOUT ANY WARRANTY; without even the implied warranty of             //
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the              //
// GNU General Public License for more details.                               //
//                                                                            //
// You should have received a copy of the GNU General Public License          //
// in the COPYING file. If not, see <http://www.gnu.org/licenses/>.           //
////////////////////////////////////////////////////////////////////////////////

///
/// \file
/// Contains the implementation of the test_visit function.
///

#include "testvisit.hpp"

////////////////////////////////////////////////////////////////////////////////
// Macro's for turning tests on and off                                       //
////////////////////////////////////////////////////////////////////////////////

/// \def TEST_KEY_WITH_ASSERTIONS
/// If this macro is defined in the testvisit.cpp file, all assertions in the
/// code will be translated to KeY. These conditions will be taken as boolean
/// expressions to prove by the KeY backend. Output will be sent to stdout.
///
/*/
#define TEST_KEY_WITH_ASSERTIONS
//*/

////////////////////////////////////////////////////////////////////////////////
// Includes                                                                   //
////////////////////////////////////////////////////////////////////////////////

#include <iostream>
using namespace std;

#include "common/assert.hpp"
#include "keysolver.hpp"
#include "navigator.hpp"
#include "tree.hpp"

////////////////////////////////////////////////////////////////////////////////
// TestVisitor Class                                                          //
////////////////////////////////////////////////////////////////////////////////

/// Visits the nodes of an abstract syntax tree to do manual testing.
///
class TestVisitor : public Navigator {
	public:
		
		VISIT_FUNCTIONS_FROM( (AssertionArea) )
};



////////////////////////////////////////////////////////////////////////////////
// Function Implementations                                                   //
////////////////////////////////////////////////////////////////////////////////

void test_visit(wptr<Node> astNode) {
	assert(astNode);
	
	sptr<TestVisitor> visitor(new TestVisitor);
	
	astNode->accept(visitor);
}

////////////////////////////////////////////////////////////////////////////////

void TestVisitor::visit(wptr<AssertionArea> node) {
	assert(node);
	
	Navigator::visit(node);
	
	#ifdef TEST_KEY_WITH_ASSERTIONS
		foreach (wptr<Expression> condition, node->conditions) {
			KeySolver solver(condition);
			cerr << "-------------------------------------------\n";
			switch (solver.status()) {
				case KeySolver::FAILED:     cerr << "FAILED";     break;
				case KeySolver::TIMEOUT:    cerr << "TIMEOUT";    break;
				case KeySolver::NOT_PROVED: cerr << "NOT PROVED"; break;
				case KeySolver::PROVED:     cerr << "PROVED";     break;
			}
			
			cerr << "\n";
			
			if (solver.status())
				cerr << "\n" << solver.report();
			
			cerr << "-------------------------------------------\n";
		}
	#endif
}
